// 
// File:   prism_ast.h
// Author: cionescu
//
// Created on March 22, 2007, 11:04 PM
//

#ifndef _prism_ast_H
#define	_prism_ast_H

#include <cstdio>
#include <vector>
#include <utility>
#include <map>

using std::vector;
using std::pair;
using std::string;
using std::map;

typedef void (*func)() visitor_type;

struct prism_ast_expr {
  token* m_token;
  
  prism_ast_expr() 
  : m_token(NULL){}
  
  prism_ast_expr(token* _token) 
  : m_token(_token) {
  print();
  }
  
  virtual void
  visit(visitor_type const& v) {
    v(m_token, NULL);
  }
  
  void
  print() const{
    if (m_token!=NULL) {
      printf("token:%s\t",m_token->get_string().c_str());
    } else printf("NULL token");
  }
};

struct prism_ast_unexpr: prism_ast_expr {
  int m_op;
  prism_ast_expr m_expr;
  
  prism_ast_unexpr(int _op, prism_ast_expr& _expr) 
  : m_op(_op), m_expr(_expr) {}
  
  void
  visit(visitor_type const& v) {
    m_expr.visit(v); 
  }
};

struct prism_ast_binexpr: prism_ast_expr {
  prism_ast_expr const& m_lexpr;
  prism_ast_expr const& m_rexpr;
  int m_op;
  
  prism_ast_binexpr(const int& _op, const prism_ast_expr& _lexpr, const prism_ast_expr& _rexpr) 
  : m_op(_op), m_lexpr(_lexpr), m_rexpr(_rexpr) {
    m_lexpr.print();
    print();
    m_rexpr.print();
  }
  
  void
  visit(visitor_type const& v) {
    m_lexpr.visit(v);
    m_lexpr.visit(v);
  }
};

struct prism_ast_update {
  typedef map<token*, prism_ast_expr> update_type;
  typedef pair<token*, prism_ast_expr> update_element_type;
  
  update_type m_update;
  
  prism_ast_update() {}
  
  prism_ast_update(update_type const& _upd)
  : m_update(_upd) {}
  
  void
  add_update(token* _name, prism_ast_expr & _expr) {
    m_update.insert(pair<token*, prism_ast_expr>(_name, _expr));
  }
};

struct prism_ast_transition {
  typedef pair<prism_ast_expr , prism_ast_update> transition_element_type;
  typedef vector<transition_element_type> transition_type;
  
  token* m_label;
  prism_ast_expr m_from;
  vector<transition_element_type> m_to;
  
  prism_ast_transition(token* _label, const prism_ast_expr& _from, const transition_type& _to)
  : m_from(_from), m_label(_label), m_to(_to) {}
  
  prism_ast_transition(){}
};

struct prism_ast_token {
  
};

struct prism_ast_variable: prism_ast_token {
  typedef std::pair<prism_ast_expr, prism_ast_expr> variable_constraint;
  
  token* m_name;
  int m_type;
  vector<variable_constraint> m_constraints;
  
  prism_ast_variable() {}
  
  prism_ast_variable(token* _name, int _type)
  : m_name(_name), m_type(_type) {}
  
  void
  push_back(variable_constraint const& _constraint) {
//    printf("new constraint on variable %s\n", m_name->get_string().c_str());
    m_constraints.push_back(_constraint);
  }
};

struct prism_ast_module: prism_ast_token {
  string m_name;
  vector<prism_ast_expr> m_init;
  vector<prism_ast_variable> m_variables;
  vector<prism_ast_transition> m_transitions;
  
  prism_ast_module() {}
  prism_ast_module(token* _name, vector<prism_ast_variable> const& _vars, vector<prism_ast_transition> const& _transitions)
  :m_variables(_vars), m_transitions(_transitions){}
  
};

struct prism_ast_formula : prism_ast_token {
  token* m_name;
  prism_ast_expr m_expr;
  
  prism_ast_formula() {}
  
  prism_ast_formula(token* _name, prism_ast_expr const&_expr)
  : m_name(_name), m_expr(_expr) {}
};

struct prism_ast_composition {
  vector<prism_ast_expr> m_compositions;
};

struct prism_ast_program {
  string m_type;
  vector<prism_ast_expr> m_init;
  vector<prism_ast_formula> m_formulae;
  vector<prism_ast_variable> m_variables;
  vector<prism_ast_module> m_modules;
  vector<prism_ast_composition> m_composition;
  
  prism_ast_program() {
    m_type = "dtmc";
  }
  
  prism_ast_program (string _name ): m_type(_name){}
};
#endif	/* _prism_ast_H */

